First and Second

Two other basic functions are First and Second, both of which take in two arguments, and do the obvious thing. They are defined:

#math88#
First~x~y = x  
Second~x~y = y  

We could, in fact, define Second in terms of Identity and First. For any x and y,
#math89#
First~Identity~x~y;SPMnbsp;;SPMnbsp;;SPMnbsp;;SPMnbsp;
  = Identity~y  
  = y  
  = Second~x~y  

So #math90#First~Identity = Second. This means that anywhere in our TEX code we have 15 we could replace it by 16. This is perhaps not the most astonishing TEX fact known to humanity, but this sort of proof did enable more complex bits of TEX to be verified before they were run.

The TEX definitions of 17 and 18 are pretty obvious.
 
Note that in TEX;SPMnbsp; 19 expands out to 20 <#103#>without<#103#> expanding out 21. This is very useful, as we can write macros that would take forever and a day to run if they expanded all their arguments, but which actually terminate quite quickly. This is called <#104#>lazy evaluation<#104#> by the functional programming community.